'''
Created on 2011-04-27

@author: kacper
'''
from dataStructs.definitions import *
from dataStructs.Transform import cnf, MultipleAnd, MultipleOr
from logger.logger import instLogFun, instLog
from test.RandomFromula import randomFormula, genFormula

log = instLog("Transform")
logFun = instLogFun(log)

termDict = {}

def getTerms(formula):
    if isinstance(formula, BinFormula):
        getTerms(formula.f1)
        getTerms(formula.f2)
        
    elif isinstance(formula, NotFormula):
        getTerms(formula.f1)
    
    else:
        termDict[formula] = 0

def countValStd(formula):
    if isinstance(formula, BinFormula):
        v1 = countValStd(formula.f1)
        v2 = countValStd(formula.f2)
        
        if isinstance(formula, AndFormula):
            return v1*v2
        elif isinstance(formula, OrFormula):
            return v1 or v2
        elif isinstance(formula, ThenFormula):
            return ( not v1 or v2)
        else:
            raise Exception("wtf")
        
    elif isinstance(formula, NotFormula):
        return not countValStd(formula.f1)
        
    else:
        return termDict[formula]

def countValCNF(formula):
    if isinstance(formula, MultipleAnd):
        y=1
        for x in formula.fs:
            y *= countValCNF(x)
        return y
    elif isinstance(formula, MultipleOr):
        y=0
        for x in formula.fs:
            y = y or countValCNF(x)
        return y
    
    elif isinstance(formula, NotFormula):
        return not countValCNF(formula.f1)
    
    return termDict[formula]

def runTest(formula):
    f0  = formula.removeThen().pushNeg()
    f1 = cnf(f0)
    val1 = countValCNF(f1)
    val2 = countValStd(formula)
    val0 = countValStd(f0)
    try:
        assert( val1 == val2 and val0 == val1 )
    except AssertionError:
        print "Assertion Error in testCNF \n AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"
        log ("Assertion Error in testCNF")
        
        log( "val1 cnf", val1,  
             "val2 ",val2,
             "val0", val0,
             "termDict " ,termDict,
             "cnf ", f1,
             "std " , formula)
        raise Exception()
    
        
        
def genVal(tab, formula):
    if tab == []:
        runTest(formula)
    else:
        term = tab[0]
        for x in [0,1]:
            termDict[term] = x
            
            genVal(tab[1:],formula)



def testCNF(formula):
    
    termDict.clear()
    tab = []
    getTerms(formula.removeThen().pushNeg())
    for x in termDict: 
        tab.append(x)
    genVal(tab,formula)
    
if __name__ == "__main__":
    for x in xrange(100):
        r = genFormula()
        print "formula gnerated" , r
        r.removeThen().pushNeg()
        print "fromula checked : " ,r
        
        testCNF(r)
                    